/*
实现功能：输入命题公式的合式公式，求出公式的真值表，并输出该公式的主合取范式和主析取范式。

输入：命题公式的合式公式

输出：公式的主析取范式和主析取范式，输出形式为：“ mi ∨ mj ; Mi ∧ Mj” ，
极小项和 ∨ 符号之间有一个空格，极大项和 ∧ 符号之间有一个空格；
主析取范式和主合取范式之间用“ ; ”隔开，“ ; ”前后各有一个空格。 
永真式的主合取范式为 1 ，永假式的主析取范式为 0 。

输入公式的符号说明：

! 非，相当于书面符号中的 “ ¬ ”

& 与，相当于书面符号中的 “ ∧ ”

| 或，相当于书面符号中的 “ ∨ ”

- 蕴含联结词，相当于书面符号中的 “ → ”

+ 等价联结词，相当于书面符号中的 “ ↔ ”

( 前括号

) 后括号
*/
/*
解题思路：
    1. 将中序表达式转换成后序表达式
        1.1 按顺序读取中序表达式
        1.2 若为操作数则直接输出
        1.3 若为左括号则直接入栈，不考虑已有符号优先级，仅在遇到右括号时才弹出输出
        1.4 若为普通操作数（非括号）则入栈。若栈顶元素优先级高于该入栈操作数则弹出（因此为便于操作将左括号优先级设为最低）
        1.5 若为右括号则依次弹出所有栈顶操作数直至遇到左括号，左括号仅弹出不输出，右括号不入栈
    2. 顺序扫描后序表达式按照计算规则进行计算
*/

#include <iostream>
#include <string>
#include <stack>
#include <set>
#include <vector>
#include <map>
#include <queue>
#include <cstring>

// #define DEBUG_OUTPUT

using namespace std;
class LogicalCalculator
{
public:
    //最终计算结果
    bool output_value;

private:
    //中缀表达式
    string in_expression;
    //后缀表达式
    string post_expression;
    //记录运算符优先级
    std::map<char, int> opt_priority;

private:
    bool cal();
    void in2post();

public:
    LogicalCalculator(/* args */);
    ~LogicalCalculator();

    void start(string input);
};

LogicalCalculator::LogicalCalculator(/* args */)
{
    opt_priority['('] = 0; //括号的情况比较特殊，不能单讲优先级。左括号直接入栈，不考虑优先级
    opt_priority['+'] = 1;
    opt_priority['-'] = 3;
    opt_priority['|'] = 4;
    opt_priority['&'] = 5;
    opt_priority['!'] = 6;
}

LogicalCalculator::~LogicalCalculator()
{
}

void LogicalCalculator::in2post()
{
//操作符栈
#ifdef DEBUG_OUTPUT
    cout << "in_expression:" << in_expression << "    ";
#endif
    stack<char> op_stack;
    for (int i = 0; i < (int)in_expression.size(); i++)
    {
        char opt = in_expression[i];
        if (opt == '0' || opt == '1') //操作数
        {
            post_expression += opt;
        }
        else //操作符
        {
            if (opt == ')')
            {
                while (!op_stack.empty())
                {
                    char tmp = op_stack.top();
                    op_stack.pop();
                    if (tmp == '(')
                        break;
                    post_expression += tmp;
                }
            }
            else if (opt == '(')
                op_stack.push(opt);
            else //判断优先级
            {
                while (true) //这里一定不能使用!op_stack.empty()作为判断项
                {
                    if (op_stack.empty())
                    {
                        op_stack.push(opt);
                        break;
                    }
                    char tmp = op_stack.top();
                    if (opt_priority[tmp] > opt_priority[opt])
                    {
                        op_stack.pop();
                        post_expression += tmp;
                    }
                    else
                    {
                        op_stack.push(opt);
                        break;
                    }
                }
            }
        }
    }
    while (!op_stack.empty())
    {
        char tmp = op_stack.top();
        op_stack.pop();
        post_expression += tmp;
    }
}

bool LogicalCalculator::cal()
{
    stack<char> opt_stack;
    stack<int> num_stack;
#ifdef DEBUG_OUTPUT
    cout << "post_expression : " << post_expression << "    ";
#endif
    for (int i = 0; i < (int)post_expression.size(); i++)
    {
        char tmp = post_expression[i];
        if (tmp == '0')
        {
            num_stack.push(0);
        }
        else if (tmp == '1')
        {
            num_stack.push(1);
        }
        else
        {
            if (tmp == '!')
            {
                int b = num_stack.top();
                num_stack.pop();
                if (b)
                    num_stack.push(0);
                else
                    num_stack.push(1);
            }
            else
            {
                int b = num_stack.top();
                num_stack.pop();
                int a = num_stack.top();
                num_stack.pop();
                int c = 0;
                switch (tmp)
                {
                case '&':
                {
                    c = a * b;
                    break;
                }
                case '|':
                {
                    if (a + b > 0)
                        c = 1;
                    else
                        c = 0;
                    break;
                }
                case '+':
                {
                    if (a == b)
                        c = 1;
                    else
                    {
                        c = 0;
                    }

                    break;
                }
                case '-':
                {
                    if (a == 1 && b == 0)
                        c = 0;
                    else
                        c = 1;
                    break;
                }
                default:
                {
                    c = 0;
                    break;
                }
                }
                num_stack.push(c);
            }
        }
    }
    if (num_stack.top() == 1)
        output_value = true;
    else
        output_value = false;
    while (!num_stack.empty())
    {
        num_stack.pop();
    }
}

void LogicalCalculator::start(string input)
{
    this->in_expression = input; //输入是中缀表达式
    in2post();                   //中缀表达式转后缀表达式
    this->cal();
    this->in_expression = "";
    this->post_expression = "";
}

string expression;
LogicalCalculator calculator;
bool out[1 << 10];
int count = 0;
int m = 0, M = 0; //
struct Directory
{
    string variable;
    bool value;
}; //存储变量以及其所代表的值

struct Directory dict[100];

int countVariable(string input);
void dfs(int level, int num_of_variables); //对变量赋值，遍历所有情况
void printOUTPUT();                        //打印输出

int main(int argc, char const *argv[])
{
    cin >> expression;
    int num_of_variables = countVariable(expression);
    // cout << num_of_variables << endl;
    memset(out, 0x0, sizeof(out));
    dfs(0, num_of_variables);
    printOUTPUT();
    return 0;
}

//计算表达式中有多少个变量
int countVariable(string input)
{
    set<string> variables; //具有重复值检查功能
    for (int i = 0, j = 0; i < (int)input.size(); i = j)
    {
        while (i < input.size())
        {
            //已知输入的变量的每个字母都是小写英文字母
            if ((int)input[i] >= 'a' && input[i] <= 'z')
                break;
            i++;
        }
        j = i;
        if (i >= input.size())
            break;
        while (j < (int)input.size() && (int)input[j] >= 'a' && input[j] <= 'z')
        {
            j++;
        }
        string tmp = input.substr(i, j - i);
        // cout << "i=" << i << ";j=" << j << endl;
        // cout << tmp << endl;
        variables.insert(tmp);
    }
    int i = 0;
    for (auto it = variables.begin(); it != variables.end(); it++, i++)
    {
        dict[i].value = false; //将变量加入字典，并赋初值
        dict[i].variable = *it;
        // cout << *it << endl;
    }

    return variables.size();
}

//对变量赋值，遍历所有情况
void dfs(int level, int num_of_variables)
{
    if (level == num_of_variables)
    {
        //进行值替换
        string tmp = expression;
        size_t pos = 0;
        for (int i = 0; i < num_of_variables; i++)
        {
            string replace_value("1");
            if (dict[i].value == false)
            {
                replace_value = "0";
            }
            // cout << i << " : " << dict[i].variable << endl;
            pos = tmp.find(dict[i].variable);

            while (pos != string::npos)
            {
                // cout << dict[i].variable << " : " << pos << endl;
                tmp.replace(pos, replace_value.size(), replace_value);
                pos = tmp.find(dict[i].variable);
            }
        }
        calculator.start(tmp); //计算
        out[count++] = calculator.output_value;
        if (calculator.output_value)
            m++;
        else
            M++;
#ifdef DEBUG_OUTPUT
        cout << tmp << " : ";
        if (calculator.output_value)
            cout << "true" << endl;
        else
            cout << "false" << endl;
#endif
        return;
    }
    dict[level].value = false;
    dfs(level + 1, num_of_variables);
    dict[level].value = true;
    dfs(level + 1, num_of_variables);
}

void printOUTPUT()
{
    string out_m = "";
    string out_M = "";
    if (m == count) //永真式
    {
        // cout << "1" << endl;
        out_M = "1";
    }
    else if (M == count) //永假式
    {
        // cout << "0" << endl;
        out_m = "0";
    }

    int i = 0;
    for (i = 0; i < count && m > 0 && M > 0; i++)
    {
        if (out[i] == true) //m
        {
            m--;
            if (m)
                out_m += "m" + to_string(i) + " ∨ ";
            else
                out_m += "m" + to_string(i);
#ifdef DEBUG_OUTPUT
                // cout << out_m << endl;
#endif
        }
        else //M
        {
            M--;
            if (M)
                out_M += "M" + to_string(i) + " ∧ ";
            else
                out_M += "M" + to_string(i);
#ifdef DEBUG_OUTPUT
                // cout << out_M << endl;
#endif
        }
    }
    for (; i < count && m; i++)
    {
        m--;
        if (m)
            out_m += "m" + to_string(i) + " ∨ ";
        else
            out_m += "m" + to_string(i);
#ifdef DEBUG_OUTPUT
            // cout << out_m << endl;
#endif
    }
    for (; i < count && M; i++)
    {
        M--;
        if (M)
            out_M += "M" + to_string(i) + " ∧ ";
        else
            out_M += "M" + to_string(i);
#ifdef DEBUG_OUTPUT
            // cout << out_M << endl;
#endif
    }
    cout << out_m << " ; " << out_M << endl;
}
